T:Type, L1,L2:(T List).
iseg(T; L1; L2)  (n:int_seg(0; (||L2|| + 1)). (L1 = firstn(n; L2))) 

latex

Definitions	prop{i:l}, t  T, P  Q, P  Q, P  Q, x:A. B(x), iseg(T; l1; l2), P  Q, x:A. B(x), T, True, Y, append(as; bs), ||as||, ff, tt, if b then t else f fi , firstn(n; as), guard(T), sq_type(T), False, A, A  B, int_iseg(i; j), int_seg(i; j), Unit, , lelt(i; j; k),
Lemmas	firstn wf, length wf1, int seg wf, append wf, length append, add functionality wrt eq, true wf, squash wf, non neg length, length zero, length firstn, assert of le int, bnot of lt int, eqff to assert, assert of lt int, eqtt to assert, iff transitivity, bnot wf, le wf, le int wf, assert wf, bool wf, lt int wf, nth tl wf, append firstn lastn